(declare-fun a () Int)
(declare-fun b () Int)
(assert (or (= a 5) (= a 7) (= a 0)))
(assert (<= (* b b) 0))
(check-sat)
